Nuprl Lemma : free-from-atom-Knd
11,40
postcript
pdf
a
:Atom1,
k
:Knd.
k
:Knd||
a
latex
Definitions
x
:
A
.
B
(
x
)
,
Knd
,
t
T
Lemmas
IdLnk
wf
,
Id
wf
,
free-from-atom-Id
,
free-from-atom-IdLnk
origin
a:Atom1, k:Knd. k:Knd||a a:Atom1, k:Knd. k:Knd||a x:A. B(x)
T